﻿/*============================================
 * 类名 :ProveTree
 * 描述 :用来操作推理树的类
 *   
 * 创建时间: 2009-11-3 15:44:32
 *============================================*/
using System;
using System.Collections.Generic;

using System.Text;
using System.Globalization;

namespace 命题证明
{
    /// <summary>证明功能的入口</summary>
    class ProveWork
    {
        #region "属性区"

        /// <summary>现在已知的所有条件，在推理的过程中这个会越来越多</summary>   
        List<ProveNode> conditions = new List<ProveNode>();

        //public List<ProveNode> Conditions
        //{
        //    get { return conditions; }
        //    set { conditions = value; }
        //}
        /// <summary>要证明的结论</summary>
        Node result;


        #endregion
        public void SetConditions( List<ProveNode> con )
        {
            conditions.Clear();
            this.conditions = con;
        }
        /// <summary>执行推理过程,若推理出结论则返回推理节点，否则返回null</summary>
        //public bool Work( List<string> con, string p )
        public ProveNode Work( Node result )
        {
            //SetCondition( con );
            this.result = result;
            while ( true )
            {
                int r = conditions.Count;
                ProveOne();
                if ( r == conditions.Count )
                    break;
                // return IsProved();
            }

            return IsProved();
        }

        /// <summary>是否已推出结论，如果已推出则返回这个已推出的节点</summary>  
        private ProveNode IsProved()
        {
            for ( int i = 0; i < conditions.Count; ++i )
            {
                //if ( conditions[i].Result.Equals( Result ) )
                if ( conditions[i].Result.AfterExpress == ExpressionFactory.ConvertToAfter( result ) )
                {
                    //已得出了结论
                    return conditions[i];

                }
            }
            return null;
        }

        /// <summary>向conditions中添加新节点</summary>
        void AddConditions( List<ProveNode> nodes )
        {
            foreach ( ProveNode n in nodes )
            {
                if ( !IsExistCondition( n.Result.AfterExpress ) && IsContain( n.Result ) )  //
                {
                    conditions.Add( n );
                }
            }
        }

        /// <summary>这个函数主要是为了考虑相似度而设，防止条件无限膨胀</summary>
        bool IsContain( Expression exp )
        {
            foreach ( ProveNode c in conditions )
            {
                //只要其中一个包含就可以了
                if ( c.Result.Contain( exp ) )
                    return true;
            }
            return false;
        }


        /// <summary>现在推出来的结论是否已经存在了，只有后序形式完全一样时才算存在</summary> 
        bool IsExistCondition( string after )
        {
            foreach ( ProveNode c in conditions )
            {
                if ( after == c.Result.AfterExpress )
                    return true;
            }
            return false;
        }


        void ProveOne()
        {
            //BinaryNumber bin = new BinaryNumber( conditions.Count );
            //当考虑定律相似度后可以将所有的条件都组合一次，用BinaryNumber实现
            for ( int i = 0; i < conditions.Count; i++ )
            {
                //只用一个条件推理               
                if ( ProveOne( new List<ProveNode> { conditions[i] } ) )
                    return;
                for ( int j = 0; j < conditions[i].Result.OperatorNodes.Count; j++ )
                {
                    if ( ProveOne( conditions[i], conditions[i].Result, j ) )
                        return;
                }
                //进行两个条件合在一起进行推理
                for ( int j = i + 1; j < conditions.Count; j++ )
                {
                    if ( ProveOne( new List<ProveNode> { conditions[i], conditions[j] } ) )
                        return;

                }
            }

        }

        /// <summary>根据一个条件，执行一次推理过程</summary>
        bool ProveOne( List<ProveNode> proves )
        {
            Expression exp = ExpressionFactory.ConvertToExpression( proves );
            //在这里对exp进行操作符的整体替代
            //又一次用这个类，进行所有情况的考虑，如果想要对"非"进行处理，那么就要对每个节点都要进行一次替换的考虑了
            //包括字母节点，不过就为这一个就要添加这样的复杂性吗
            MatchLaw m = new MatchLaw();
            //用二进制数依次遍历所有的情况

            for ( int i = 0; i < Math.Pow( 2, exp.OperatorNodes.Count ); i++ )
            {
                ReplaceWork replace = new ReplaceWork( exp );
                replace.Replace( i );
                //TODO:在这里进行条件节点上的判断
                //将变形后的形式和公式进行对比
                AddConditions( m.MatchProof( replace, proves ) );
                AddConditions( m.MatchEqual( replace, proves ) );
            }


            if ( IsProved() != null )
                return true;
            return false;
        }

        bool ProveOne( ProveNode prove, Expression old, int j )
        {
            Expression exp = new Expression( ExpressionFactory.ConvertToMiddle( old.OperatorNodes[j] ) );
            MatchLaw m = new MatchLaw();
            for ( int i = 0; i < Math.Pow( 2, exp.OperatorNodes.Count ); i++ )
            {
                ReplaceWork replace = new ReplaceWork( exp );
                replace.Replace( i );

                AddConditions( m.MatchEqual( replace, new List<ProveNode>() { prove } ), old, j );
            }
            if ( IsProved() != null )
                return true;
            return false;
        }

        private void AddConditions( List<ProveNode> list, Expression old, int j )
        {
            foreach ( ProveNode n in list )
            {
                Expression exp = old.Clone();
                if ( exp.OperatorNodes[j].Parent == null )
                {
                    exp.Head = n.Result.Head;
                }
                else if ( exp.OperatorNodes[j].Parent.Left == exp.OperatorNodes[j] )
                {
                    exp.OperatorNodes[j].Parent.Left = n.Result.Head;
                }
                else
                {
                    exp.OperatorNodes[j].Parent.Right = n.Result.Head;
                }

                n.Result = new Expression( ExpressionFactory.ConvertToMiddle( exp.Head ) );
                AddConditions( new List<ProveNode> { n } );
            }
        }


    }
}
